package main;
import main.LiteralAlocatorAndMap;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.util.Date;
import java.util.Vector;


import utils.IOUtils;
import utils.MatrixUtils;
import utils.StreamGobbler;


public class Main {
	public static String COMMON_FILE_NAME = "Lefel_Zilberman/extermal_";
	public static final String NO_SOL_MSG = "NOSOL";
	
	public static int run(String[] args){
		new File("./Lefel_Zilberman").mkdir();

		int numOfVertices = 4;
		boolean output = true;
		if (args.length > 0){
			numOfVertices = Integer.parseInt(args[0]);
		}
		if (args.length > 1){
			numOfVertices = Integer.parseInt(args[0]);
			output = Boolean.parseBoolean(args[1]);
		}
		File instanceFile = IOUtils.generateInstanceFile(numOfVertices, COMMON_FILE_NAME + numOfVertices + ".instance");
		
		Solution sol = getMaxEdgesSolution(instanceFile);
		if (output && sol != null){
			System.out.println("f4(" + numOfVertices + ")=" + sol.getNumOfEdges());
			System.out.println();
			System.out.println(MatrixUtils.print(sol.getEdges()));
		}
		boolean verified = Verifier.verify(sol.getEdges());
		
		if (verified){
			String solFileName = COMMON_FILE_NAME + numOfVertices +".sol";
			IOUtils.generateSolFile(solFileName, sol);
			
			String dotFilePath = COMMON_FILE_NAME + numOfVertices +".dot";
			IOUtils.generateDotFile(dotFilePath,sol.getEdges());
			try{
				//generating png file - visualizing the solution
				Process pr = execut("dot","-Tpng","-O", new File(dotFilePath).getAbsolutePath());
				int err = pr.waitFor();
				if (output){
					//open the png file
					pr = execut("cmd.exe","/c","start",new File(dotFilePath + ".png").getAbsolutePath());
				}
			}catch(Exception e){
				e.printStackTrace();
			}
			return sol.getNumOfEdges();
		}
		else{
			if (output)
				System.out.println("ERROR IN SOLUTION!!");
			return 0;
		}
	}
	
	public static void main(String[] args) {
		run(args);
	}
	
	private static int readInstanceFile(File instanceFile){
		int numOfVertices = -1;
		try{
			BufferedReader br = new BufferedReader(new FileReader(instanceFile));
			String line = br.readLine();
			String[] tokens = line.split(" ");
			numOfVertices = Integer.parseInt(tokens[1]);
		}
		catch(IOException ioex){
			ioex.printStackTrace();
		}
		return numOfVertices;
	}
	
	private static Vector<int[]> generateClauses(LiteralAlocatorAndMap map){
		Vector<int[]> cnf = new Vector<int[]>();
		
		// Generate map and clauses "tying" the values above and below diagonal.
		Vector<int[]> mapGenerationCnf = map.generateMap();
		int zeroLit = map.getZeroLit();
		mapGenerationCnf.add(new int[]{-zeroLit});
		
		cnf.addAll(mapGenerationCnf);
		
		// Add no circles of size 4 cnf
		cnf.addAll(Encoder.circles(map));
		
		//Add sums cnf
		int[] edgeLiterals = map.getEdgeLiterals();
		int[] edgeLitsCopy = new int[edgeLiterals.length];
		for (int i = 0; i < edgeLiterals.length; i++){
			edgeLitsCopy[i] = -edgeLiterals[i];
		}
		Vector<int[]> sumCnf = new Vector<int[]>();
		int[] sumBits = Encoder.fullAdder(edgeLitsCopy, map, sumCnf);
		map.setSumBits(sumBits);
		
		cnf.addAll(sumCnf);
		
		cnf.addAll(Encoder.optimizations(map));
		
		return cnf;
	}
	
	private static Solution getMaxEdgesSolution(File instancefile )  {
		int numOfVertices = readInstanceFile(instancefile);
		LiteralAlocatorAndMap map = new LiteralAlocatorAndMap(numOfVertices);
		
		Vector<int[]> cnf = generateClauses(map);
		int[] sumBits = map.getSumBits();
		
		String mapFileName = COMMON_FILE_NAME + numOfVertices + ".map";
		IOUtils.generateMapFile(mapFileName, map.getLiteralsToEdgesMap(), sumBits);
		
		String scriptFileName = COMMON_FILE_NAME + numOfVertices + ".script";
		IOUtils.generateScriptFile(scriptFileName, cnf, sumBits);
		
		try {
			String satFilePath = COMMON_FILE_NAME + numOfVertices + ".sat";
			Date start = new Date();
			Process pr = execut("lib/SCryptoMinisatWin64.exe", COMMON_FILE_NAME + numOfVertices + ".script",  satFilePath);
			int err = pr.waitFor();
			Date end = new Date();
			System.out.println("Time to solve f4(" + numOfVertices + ") -> " + (end.getTime()-start.getTime()));
			Solution sol = Decoder.getSolution(satFilePath, map);
			return sol;
			
		} catch (Exception e) {
			e.printStackTrace();
		}
		
		return null;
	}


	private static Process execut(String ... cmd) throws IOException {
		ProcessBuilder pb;
		Process pr;
		pb = new ProcessBuilder(cmd);
		pb.redirectErrorStream(true);
		pr = pb.start();
		StreamGobbler.gobble(pr.getInputStream());
		return pr;
	}


	



	
}
